Lemme d'échange de Steinlitz :
Soit \(L=\{e_1,\ldots,e_k\}\) un système libre dans \(E\) et \(G=\{g_1,\ldots,g_p\}\) un système générateur de \(E\) (\(\operatorname{Vect}(g_1,\ldots,g_p)=E\))
Alors \(p\geqslant k\) et il existe une permutation \(\sigma\) de \(\{1,\ldots,p\}\) telle que \(\{e_1,e_k,g_{\sigma(k+1)},\ldots,g_{\sigma(1)}\}\) est générateur
(Famille libre - Famille linéairement indépendante, Famille génératrice, Permutation)
Lemme de Steinlitz :
Soit \(L\) un système libre et \(G\) un système générateur
Alors il existe une application injective \(f:L\to G\) tel que \(G\setminus f(L)\cup L\) est un système générateur
(Famille génératrice, Famille libre - Famille linéairement indépendante, Injection)